/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

package chameleon.model.NuGatManager;

import chameleon.model.NuGatStructure.symbTable.SymbTable;
import chameleon.model.NuGatStructure.prop.PropGame;
import chameleon.model.NuGatStructure.prop.PropDbGame;
import chameleon.model.NuGatStructure.opt.Opt;
import chameleon.model.NuGatStructure.utils.Node;
import chameleon.model.NuGatStructure.fsm.GameBddFsm;
import chameleon.model.NuGatStructure.strategy.StructCheckLTLGameSF07;
import chameleon.model.NuGatStructure.strategy.GameStrategy;
import chameleon.model.NuGatManager.Strategy.PreImage;
import chameleon.model.NuGatManager.Strategy.PreImageComputation;
import chameleon.model.NuGatManager.Strategy.SafetyStrategyComputation;
import chameleon.gameSolver.NuGat.NuGatInterface;
import chameleon.model.AbstractManager;
import chameleon.model.GameFactory;
import chameleon.model.NuGatManager.Strategy.GenReactivityBuchiGameStrategyComputation;
import chameleon.model.NuGatManager.Strategy.LtlGameSFO7Computation;
import chameleon.model.transitionFormat.AbstractTransition;
import chameleon.model.winningCondition.Tag;
import chameleon.model.winningCondition.WinningCondition;
import chameleon.model.winningCondition.WinningConditionFactory;
import chameleon.view.OutputManager;
import chameleon.view.input.Input;
import com.sun.jna.Native;
import java.io.File;
import java.io.IOException;
import java.util.logging.Level;
import java.util.logging.Logger;

/**
 *
 * This class execute the action in link with the game Solver NuGat. Certains
 * functions are just a wrapper to NuGat and other function add new functionalities.
 *
 * @author simon
 */
public class NuGatManager extends AbstractManager {

    private NuGatInterface nugat_;

    //*************** CONSTRUCTOR *****************************************//

    public NuGatManager(Input input){
        super(input,input.getToolName());
    }
    
    //*************** CHAMELEON COMMANDS **********************************//

    /**
     * This function builds the game Structure in class @Chameleon.model.game.
     */

    @Override
    public void createGame(){
        try {
            transferFile2GameStructure();
        } catch (IOException ex) {
            Logger.getLogger(NuGatManager.class.getName()).log(Level.SEVERE, null, ex);
        }
    }

    /**
     * This method calls NuGat function to solve the game and put the strategies
     * in file. These files are stored in strategy folder.
     */

    @Override
    public void solveGame() {
        checkAllProperty();
    }

    @Override
    public File getResult() {
        throw new UnsupportedOperationException("Not supported yet.");
    }

    /**
     * This function convert a game on java structure (@Chameleon.model.game) to
     * a NuGat game structure. The following actions are mandatory :
     *
     *  -set input file in NuGat
     *  -build the flat hierarchy
     *  -encode variables
     *  -build the model
     *  -build the boolean model.
     *
     * After these conversion to NuGat structure the bdd Fsm are stored.(see
     * addBddFsm2GameStructure()).
     */

    public void buildGame(){
        try {
            String fileName = game_.getSmvFile().getFile().getPath();
            nugat_ = (NuGatInterface) Native.loadLibrary("monster", NuGatInterface.class);
            game_.setNuGatInterface(nugat_);
            initNuGat(fileName);
            setInputFile(fileName);
            buildFlatHierarchy();
            encodeVariables();
            buildModel();
            buildBooleanModel();
            addBddFsm2GameStructure();
            
            /*Variable var = new Variable("test1", 0, 1);
            Vector<Variable> vars = new Vector<Variable>();
            vars.add(var);
            Player player = new Player(1, vars, null);
            player.addPlayer(nugat_, game_);
            
            
            /*GameBddFsm game = game_.getGameBddFsm();
            BddFsm player1 = game.getTransitionRelationPlayer1();
            Bdd trans = player1.getMonolithicTransBdd();
            Bdd init = player1.getInitStates();
            
            SymbTable st = game_.getGlobalSymbTable();
            NodeList vars = st.getVars();
            Node transNode = new Node(nugat_.BddEnc_bdd_to_wff(game_.getBddEncoding().ptr(),
                    init.ptr(), vars.ptr()),nugat_);
            
            System.out.println("node"+transNode.sprintNode());
            
            Node var = vars.NodeListToNode();
            System.out.println("vars : "+var.sprintNode());*/
            GameBddFsm game = game_.getGameBddFsm();
            game.printInfo("lockGameFsm.info");
            

        } catch (IOException ex) {
            Logger.getLogger(NuGatManager.class.getName()).log(Level.SEVERE, null, ex);
        }
    }

    public void quitCmd(){
        nugat_.Game_quit_cmd();
        nugat_.Game_Quit();
    }

    private void transferFile2GameStructure() throws IOException {
        //Now a Game can only contains one file!
        //Here we convert this file into a game structure

        File smvModel = input_.getSmvFile().getFile();
        game_ = GameFactory.createGame(smvModel);


    }

    public void writeFlatModel(){
        String[] argv = {"write_flat_model"};
        nugat_.CommandGameWriteModelFlat(argv.length, argv);
    }

    /**
     * This function store the gameBddFsm, and the two BddFsm in a GameBddFsmDecorator in
     * @Chameleon.model.game .
     */

    private void addBddFsm2GameStructure(){
        //add Game Bdd Fsm from NuGat at our game structure
       PropDbGame propDbGame = game_.getPropDatabase();
       
       
       GameBddFsm gameBddFsm = new GameBddFsm(propDbGame.getGameBddFsm(), nugat_);

       game_ = GameFactory.addGameBddFsm(game_, gameBddFsm);

    }

    //********************** COMPUTE PREIMAGE *****************************//

    /**
     * This function computes the Pre-Image for a given condition. A condition
     * is Property player target.
     * Property : REACHTARGET, REACHDEADLOCK, AVOIDTAGET, AVOIDDEADLOCK
     * Player : PLAYER_1, PLAYER_2
     * Target : Set of states
     */

    public PreImage computePreImage(WinningCondition wc){
         PreImageComputation computePreImage = new PreImageComputation(nugat_, 
                 wc.getPropGame());
         
         PreImage preImage = computePreImage.compute(game_.getBddEncoding(),
                                                    game_.getOptsHandlerInstance(),
                                                    game_.getGameBddFsm());
         
         return preImage;
    }
    
    public PreImage computePreImage(String[] param){
         WinningConditionFactory factory = new WinningConditionFactory();
         WinningCondition wc = factory.constructWinningCondition(nugat_, param, game_.getPropDatabase());
         PreImageComputation computePreImage = new PreImageComputation(nugat_, 
                 wc.getPropGame());
         
         PreImage preImage = computePreImage.compute(game_.getBddEncoding(),
                                                    game_.getOptsHandlerInstance(),
                                                    game_.getGameBddFsm());
         
         return preImage;
    }
    
    //************************* COMPUTE STRATEGY **************************//
    
    public void computeStrategy (String[] param){
        WinningConditionFactory factory = new WinningConditionFactory();
        WinningCondition wc = factory.constructWinningCondition(nugat_, param, game_.getPropDatabase());
        PropGame prop = wc.getPropGame();
        OutputManager output = new OutputManager();
        
        
        Node expr = new Node(prop.getExprCore().ptr(),nugat_);
        output.displayString("Property verified : "+prop.getPlayer()+" "+expr.sprintNode()+"\n");
        
        GameStrategy strategy = null;
        if (wc.getPropertyKind() == Tag.AVOIDDEADLOCK || 
                wc.getPropertyKind() == Tag.AVOIDTARGET ||
                wc.getPropertyKind() == Tag.REACHDEADLOCK ||
                wc.getPropertyKind() == Tag.REACHTARGET){
            PreImage preImage = computePreImage(wc);
            SafetyStrategyComputation strat = new SafetyStrategyComputation(nugat_, preImage, game_);
            strategy = strat.computeStrategy();
        }
        else if (wc.getPropertyKind() == Tag.GENREACTIVITY){   
            
            GenReactivityBuchiGameStrategyComputation strat = new GenReactivityBuchiGameStrategyComputation(prop, true,game_, nugat_);
            strategy = strat.checkGenReactivitySpec();
        }
        else if (wc.getPropertyKind() == Tag.BUCHIGAME){
            
            GenReactivityBuchiGameStrategyComputation strat = new GenReactivityBuchiGameStrategyComputation(prop, true,game_, nugat_);
            strategy = strat.checkBuchiGameSpec();
            
        }
        else if (wc.getPropertyKind() == Tag.LTLGAME){
            
            LtlGameSFO7Computation strat = new LtlGameSFO7Computation(prop,game_, nugat_);
            strategy = strat.checkLtlGameSF07();
            
            //game_ = GameFactory.addCls(game_, strategy);
        }
        else
            throw new RuntimeException("Unknow kind of game");
        

        game_ = GameFactory.addStrategy(game_, strategy);
        game_ = GameFactory.addInitStrategy(game_, strategy);
        strategy.printStatus();
    }

    public void computeLtlStrategy(String[] param) {
        WinningConditionFactory factory = new WinningConditionFactory();
        WinningCondition wc = factory.constructWinningCondition(nugat_, param, game_.getPropDatabase());
        
        OutputManager output = new OutputManager();
        PropGame prop = wc.getPropGame();
        Node expr = new Node(prop.getExprCore().ptr(),nugat_);
        output.displayString("Property verified : "+prop.getPlayer()+" "+expr.sprintNode()+"\n");
            
        LtlGameSFO7Computation strat = new LtlGameSFO7Computation(prop,game_, nugat_);
        
        int i=4;
        
        while (i < param.length){
            String[] arg = param[i].split(" ");
            if (arg[0].equals("k")){
                Integer kmin = new Integer(arg[1]);
                strat.setKmin_(kmin);
            }
            else if (arg[0].equals("K")){
                Integer kmax = new Integer(arg[1]);
                strat.setKmax_(kmax);
            }
            else if (arg[0].equals("w")){
                if(arg[1].equals("p"))
                    strat.setW(nugat_.GAME_WHO_PROTAGONIST);
                else if (arg[1].equals("a"))
                    strat.setW(nugat_.GAME_WHO_ANTAGONIST);
                else if (arg[1].equals("b"))
                    strat.setW(nugat_.GAME_WHO_BOTH);
                else if (arg[1].equals("1"))
                    strat.setW(nugat_.GAME_WHO_PLAYER_1);
                else if (arg[1].equals("2"))
                    strat.setW(nugat_.GAME_WHO_PLAYER_2);
                else
                    throw new RuntimeException("Unknow parameter for compute_ltl_strategy command!");
            }
            else
                throw new RuntimeException("Unknow parameter for compute_ltl_strategy command!");
            ++i;
        }
        
        
        StructCheckLTLGameSF07 cls = strat.checkLtlGameSF07();
            
        /*strategy = cls.getStrategy();
        strategy.setStatus(prop.getStatus());
        strategy.setProp(prop);*/
            
        game_ = GameFactory.addStrategy(game_, cls);
        game_ = GameFactory.addInitStrategy(game_, cls);
        game_ = GameFactory.addCls(game_, cls);
        
        cls.printStatus();
    }
    
    public void printStrategy(String file){
        GameStrategy strategy = game_.getStrategy();
        /*if(strategy.getType() == nugat_.PropGame_LtlGame){
            StructCheckLTLGameSF07 cls = game_.getCls();
            cls.printStrategy(file, game_.getOptsHandlerInstance());
        }
        else*/
            strategy.printStrategy(file);
    }
    
    public void modifyOrderStrategy(String orderFile){
        GameStrategy strategy = game_.getStrategy();
        System.out.println("size before : "+strategy.getSize());
        strategy.modifyVarOrder(orderFile, game_.getBoolEncoding(),
                game_.getOptsHandlerInstance());
        
        System.out.println("size after : "+strategy.getSize());
    }

    public void checkIfStrategyIsWinning() throws IOException{
        GameStrategy strategy = game_.getStrategy();
        strategy.strategyIsWinning(game_);        
    }
    
    //*************** NUGAT COMMANDS ***************************************//

    /**
     * This function initialise NuGaT. It prepares NuGaT to the reading
     * of the Smv file given in paramater.
     * @param fileName
     * @throws IOException
     */
    private void initNuGat(String fileName) throws IOException{
       nugat_.Smgame_Init();

       //Behavior of sm_ParseLineOptions for -int
       Opt opt = game_.getOptsHandlerInstance();
       opt.setPgmPath(fileName);
       opt.unsetBatch();


       nugat_.init_options_cmd();
       nugat_.Sm_NusmvrcSource();
       nugat_.Parser_Init();
    }

    private void setInputFile(String fileName) {
       nugat_.Parser_ReadSMVFromFile(fileName);

       //Insert model in NuGat
       Opt opt = game_.getOptsHandlerInstance();
       opt.setInputFile(fileName);
    }

    private void buildFlatHierarchy() {
        if (nugat_.Game_CommandFlattenHierarchy()==1)
           try {
            throw new IOException("flatten_hierarchy error");
        } catch (IOException ex) {
            Logger.getLogger(NuGatManager.class.getName()).log(Level.SEVERE, null, ex);
        }
    }

    private void encodeVariables() {
       nugat_.util_getopt_reset();
       nugat_.Game_CommandEncodeVariables(null);
    }

    private void buildBooleanModel() {
        String[] argv = {"build_boolean_model"};
        nugat_.CommandGameBuildBooleanModel(argv.length, argv);
    }

    /**
     * WARNING : Not used anymore
     */

    private void buildBddModel() {
       /*Pointer st = nugat_.Compile_get_global_symb_table();
       Pointer scalar_fsm =
               nugat_.getGameScalarSexpFsm(
               nugat_.PropPkg_get_prop_database());

       Pointer bdd_fsm = nugat_.Game_CreateGameBddFsm(nugat_.Compile_get_global_fsm_builder(),
               nugat_.Enc_get_bdd_encoding(),
               scalar_fsm,
               nugat_.SymbTable_get_layer(st, nugat_.LAYER_PLAYER_1),
               nugat_.SymbTable_get_layer(st, nugat_.LAYER_PLAYER_2),
               nugat_.getPartitionMethod(nugat_.OptsHandler_get_instance()));

       nugat_.setGameBddFsm(nugat_.PropPkg_get_prop_database(), bdd_fsm);
       //add Bdd Fsm from NuGat at our game structure
       GameBddFsmDecorator gameBddFsm = new GameBddFsmDecorator(nugat_.getGameBddFsm
               (nugat_.PropPkg_get_prop_database()));
       game_.addDecoration(gameBddFsm);*/
    }

    private void checkAllProperty() {
        checkReachDeadlock(argv("check_reach_deadlock"));
        checkReachTarget(argv("check_reach_target"));
        checkAvoidTarget(argv("check_avoid_target"));
        checkAvoidDeadlock(argv("check_avoid_deadlock"));
        checkBuchiGame(argv("check_buchi_game"));
        checkGenReactivity(argv("check_gen_reactivity"));
        checkLtlGame(argv("check_ltlgame_sf07"));
    }
    
    private String[] argv(String arg){
        String[] argt = {arg};
        return argt;
    }

    private void buildModel() {
        String[] argv = {"build_model"};
        nugat_.CommandGameBuildModel(argv.length, argv);
    }

    public void checkReachTarget(String[] argv){
        nugat_.game_invoke_game_command(argv.length, argv, nugat_.PropGame_ReachTarget);
    }

    public void checkReachDeadlock(String[] argv){
        nugat_.game_invoke_game_command(argv.length, argv, nugat_.PropGame_ReachDeadlock);
    }

    public void checkAvoidTarget(String[] argv) {
        nugat_.game_invoke_game_command(argv.length, argv, nugat_.PropGame_AvoidTarget);
    }

    public void checkAvoidDeadlock(String[] argv) {
        nugat_.game_invoke_game_command(argv.length, argv, nugat_.PropGame_AvoidDeadlock);
    }

    public void checkBuchiGame(String[] argv) {
        nugat_.game_invoke_game_command(argv.length, argv, nugat_.PropGame_BuchiGame);
    }
    
    public void checkGenReactivity(String[] argv) {
        nugat_.game_invoke_game_command(argv.length, argv, nugat_.PropGame_GenReactivity);
    }

    public void checkLtlGame(String[] argv){
        nugat_.CommandCheckLtlGameSpecSF07(argv.length, argv);
    }

    public void writeOrder(String[] argv){
        nugat_.CommandWriteOrder(argv.length, argv);
    }
    
    public void showVars(String[] argv){
        nugat_.CommandShowVars(argv.length, argv);
    }
    //****************** ADD TRANSITION ************************************//

    /**
     * This function add the transition given on input to the Game.
     * 
     * @param player
     * @param transition
     * @param mapTable
     * @return
     */

    public NuGatManager addTransition(int player, AbstractTransition transition) {
        AddTransitionFactory factory = new AddTransitionFactory(nugat_, game_);
        nugat_ = factory.addTransition(player, transition);

        return this;
    }

    //****************** ADD NEW VARIABLE **********************************//
    
    
    /**
     * This function can add a new boolean or bound integer value variable in the
     * symbol table.
     * @param player
     * @param varName
     * @param type
     * @param lowerBound
     * @param higherBound
     * @return 
     */
    
    public NuGatManager addIntVariable(int player, String varName, int lowerBound,
            int higherBound){
        
        SymbTable st = game_.getGlobalSymbTable();
        st.addIntVariable(varName, player, lowerBound, higherBound);
        
        //game_.getBoolEncoding().commitLayer(layer);
        //game_.getBddEncoding().commitLayer(layer);
        
        
        return this;
    }
    
    
    //****************** QUANTIFY VARIABLE OUT OF THE STRATEGY**************//

    public void extractSubset(String maskFileName) throws IOException {
         GameStrategy strategy = game_.getStrategy();
         System.out.println("size before : "+strategy.getSize());
         strategy.extractSubset(maskFileName);
         System.out.println("size after : "+strategy.getSize());
    }
    
    //****************** RESTORE INITIAL STRATEGY *************************//
    
    public void restoreInitStrategy(){
        GameStrategy initStrategy = game_.getInitStrategy();
        GameFactory factory = new GameFactory();
        game_ = factory.deleteStrategy(game_);
        game_ = factory.addStrategy(game_, initStrategy);
    }

}